#include "Minisat.h"
#include <iostream>
#include <fstream>
#include <cstdlib>

/***************** minisat ******************/
/* private */
SAT* Minisat::VC2SAT(Graph g) {
	int nb_vertex = g.getNbVertex();
	SAT* s = new SAT();
	vector<int> neighbours;
	s->setNbVariables(nb_vertex);

	for (int i=0; i<nb_vertex; i++) {
		neighbours = g.getNeighbours(i);
		for (int j=0; j<neighbours.size(); j++) {
			s->add(i+1,neighbours[j]+1);
		}
	}
	return s;
}

vector<int> Minisat::SAT2VC(SAT* s) {
	vector<int> ret = vector<int>();
	vector<int> solution = s->getSolution();
	for (int i=0; i < solution.size(); i++) {
		int x = solution[i];
		if (x > 0)
			ret.push_back(x);
	}
	return ret;
}

/* constructeur/destructeur */
Minisat::Minisat(){
	_sat = NULL;
}

Minisat::Minisat(Graph g){
	setProblem(g);
}

Minisat::~Minisat() {
	delete(_sat);
}

/* fonctions */
void Minisat::setProblem(Graph g) {
	_sat = VC2SAT(g);
}

void Minisat::eval() {
	_sat->eval();
}

vector<int> Minisat::getSolution() {
	return SAT2VC(_sat);
}

vector<int> Minisat::runMinisatOn(Graph g) {
	setProblem(g);
	eval();
	return getSolution();
}

/******************* SAT ********************/
SAT::SAT() {
	_evaluated = false;
	_solvable = false;
	_nb_variables = 0;
	_problem = vector<pair<int,int> >();
	_solution = vector<int>();
}

SAT::SAT(vector<pair<int,int> > v) {
	SAT();
	for(int i=0; i<v.size(); i++)
		add(v[i]);
}

SAT::~SAT() {
}

void SAT::add(pair<int,int> p) {
	_problem.push_back(p);
}

void SAT::add(int a, int b) {
	_problem.push_back(pair<int,int>(a,b));
}

void SAT::setNbVariables(int n) {
	_nb_variables = n;
}

int SAT::getNbVariables() {
	return _nb_variables;
}

vector<int> SAT::getSolution() {
	if (_evaluated) {
		return _solution;
	} else {
		cerr << "Error : trying to get a solution of a non-evaluated SAT problem" << endl;
		return vector<int>();
	}
}

void SAT::eval() {
	writeInfile();
	runMinisat();
	readOutfile();
}

void SAT::writeInfile() {

	ofstream out ("in", ios_base::out | ios_base::trunc);

	out << "c input file auto-generated to be evaluated by minisat" << endl;
	out << "p cnf " << _nb_variables << " " << _problem.size() << endl;

	for (int i=0; i<_problem.size(); i++) {
		out << _problem[i].first;
		out << " ";
		out << _problem[i].second;
		out << " 0\n";
	}

	out.close();
}
//TODO
void SAT::runMinisat() {
	system("./minisat_static -verb=0 in out");
	_evaluated = true;
}

void SAT::readOutfile() {
	ifstream in ("out", ios_base::in);

	string sat;
	in >> sat;

	int i;
	while(in.good()) {
		in >> i;
		if (i>0) {
			_solution.push_back(i);
		}
	}

	in.close();
}

bool SAT::evaluated() {
	return _evaluated;
}

bool SAT::solvable() {
	return _solvable;
}
